or(x, x) → x
and(x, x) → x
not(not(x)) → x
not(and(x, y)) → or(not(x), not(y))
not(or(x, y)) → and(not(x), not(y))
↳ QTRS
↳ DependencyPairsProof
or(x, x) → x
and(x, x) → x
not(not(x)) → x
not(and(x, y)) → or(not(x), not(y))
not(or(x, y)) → and(not(x), not(y))
NOT(and(x, y)) → NOT(y)
NOT(or(x, y)) → NOT(x)
NOT(and(x, y)) → NOT(x)
NOT(or(x, y)) → AND(not(x), not(y))
NOT(or(x, y)) → NOT(y)
NOT(and(x, y)) → OR(not(x), not(y))
or(x, x) → x
and(x, x) → x
not(not(x)) → x
not(and(x, y)) → or(not(x), not(y))
not(or(x, y)) → and(not(x), not(y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
NOT(and(x, y)) → NOT(y)
NOT(or(x, y)) → NOT(x)
NOT(and(x, y)) → NOT(x)
NOT(or(x, y)) → AND(not(x), not(y))
NOT(or(x, y)) → NOT(y)
NOT(and(x, y)) → OR(not(x), not(y))
or(x, x) → x
and(x, x) → x
not(not(x)) → x
not(and(x, y)) → or(not(x), not(y))
not(or(x, y)) → and(not(x), not(y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
NOT(and(x, y)) → NOT(y)
NOT(or(x, y)) → NOT(x)
NOT(and(x, y)) → NOT(x)
NOT(or(x, y)) → NOT(y)
or(x, x) → x
and(x, x) → x
not(not(x)) → x
not(and(x, y)) → or(not(x), not(y))
not(or(x, y)) → and(not(x), not(y))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
NOT(and(x, y)) → NOT(y)
NOT(and(x, y)) → NOT(x)
Used ordering: Polynomial interpretation [25,35]:
NOT(or(x, y)) → NOT(x)
NOT(or(x, y)) → NOT(y)
The value of delta used in the strict ordering is 27/8.
POL(NOT(x1)) = (3/2)x_1
POL(or(x1, x2)) = (11/4)x_1 + (4)x_2
POL(and(x1, x2)) = 9/4 + x_1 + (5/4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
NOT(or(x, y)) → NOT(x)
NOT(or(x, y)) → NOT(y)
or(x, x) → x
and(x, x) → x
not(not(x)) → x
not(and(x, y)) → or(not(x), not(y))
not(or(x, y)) → and(not(x), not(y))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
NOT(or(x, y)) → NOT(x)
NOT(or(x, y)) → NOT(y)
The value of delta used in the strict ordering is 1/2.
POL(NOT(x1)) = (2)x_1
POL(or(x1, x2)) = 1/4 + (5/2)x_1 + (5/2)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
or(x, x) → x
and(x, x) → x
not(not(x)) → x
not(and(x, y)) → or(not(x), not(y))
not(or(x, y)) → and(not(x), not(y))